es:ES, i, x:Id, P:({e:E| loc(e) = i }Prop), ds:x:Id fp Type, f:(State(ds)ds(x)?Top).
es-update-iff(es;i;x;ds;e.P(e);s.f(s))  Prop 

latex

Definitions	ES, t  T, Id, Prop, x:A. B(x), loc(e), E, x. t(x), a:A fp B(a), Top, IdDeq, State(ds), f(x)?z, vartype(i;x), x when e, (x after e), x(s), A, P  Q, state@i, (state when e), P & Q, e@i. P(e), A & B, es-update-iff(es;i;x;ds;e.P(e);s.f(s))
Lemmas	alle-at wf, es-state-when wf, subtype rel dep function, subtype rel self, not wf, es-after wf, es-when wf, es-vartype wf, decl-state wf, fpf-cap wf, id-deq wf, top wf, fpf wf, es-E wf, es-loc wf, Id wf, event system wf